﻿using System;
using System.Collections;
using System.Collections.Generic;
using System.Collections.Specialized;
using System.ComponentModel;
using System.Diagnostics;
using System.IO;
using System.Linq;
using System.Text;
using System.Threading;
using System.Threading.Tasks;

using agree.schema;

using alib.BitArray;
using alib.Collections;
using alib.Collections.ReadOnly;
using alib.Combinatorics;
using alib.Debugging;
using alib.Enumerable;
using alib.Reflection;
using alib.String;

namespace agree.transfer_prototype
{
	[DebuggerDisplay("{ToString(),nq}")]
	public abstract class type_base
	{
		static int next_id;
		public static bool IsVar(String s)
		{
			int q;
			if (s.Length == 1 || int.TryParse(s.Substring(1), out q))
			{
				return s[0] == 'h' || s[0] == 'x' || s[0] == 'e';
			}
			return false;
		}

		protected type_base(String value)
		{
			this.id = Interlocked.Increment(ref next_id) - 1;
			this.s = value;
		}

		[DebuggerBrowsable(DebuggerBrowsableState.Never)]
		protected int id;

		[DebuggerBrowsable(DebuggerBrowsableState.Never)]
		protected readonly String s;

		public String Type { get { return s; } }

		public abstract String SkolemTag { get; }

		public override String ToString() { return this.SkolemTag; }
	};


	[DebuggerDisplay("{ToString(),nq}")]
	public sealed class Var : type_base
	{
		public Var(String s)
			: base(s)
		{
			Debug.Assert(IsVar(s));
		}
		public override String SkolemTag
		{
			get { return s + id; }
		}
	};

	[DebuggerDisplay("{ToString(),nq}")]
	public sealed class type : type_base
	{
		public type(String s)
			: base(s)
		{
		}

		public override String SkolemTag
		{
			get
			{
				//return s;
				return s + "-" + id;
			}
		}
		public override string ToString()
		{
			return s + "-" + id;
		}
	};
}